
; Copyright (c) 2015 Microsoft Corporation

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)

(assert (! (<= 0 a) :named a-lower))
(assert (! (<= a 1) :named a-upper))
(assert (! (<= 0 b) :named b-lower))
(assert (! (<= b 1) :named b-upper))
(assert (! (<= 0 c) :named c-lower))
(assert (! (<= c 1) :named c-upper))
(assert (<= 0 d))
(assert (<= d 1))
(assert (! (<= (+ a b d) 1) :named at-most-one))
(assert (! (or (= (+ (* 2 a) c) 1)
               (= (+ a (* 2 d)) 1))
           :named complex))
(apply simplify :print-dependencies true)
(echo "after solving...")
(apply (and-then simplify solve-eqs) :print-dependencies true)
(echo "with pb2bv")
(apply (and-then simplify solve-eqs pb2bv simplify) :print-dependencies true :print-model-converter true)
